@${\it loc}$ $x$ initially $v$:$T$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr(inr(inl($\langle$${\it loc}$$,\,$$T$$,\,$$x$$,\,$$v$$\rangle$)))